@rnd = float<ieee_64,ne>;

x0 = rnd(x0_);
x1 = rnd(x1_);
x2 = rnd(x2_);
x3 = rnd(x3_);
x4 = rnd(x4_);

c0 = rnd(-0.793176);
c1 = rnd(0.154365);
c2 = rnd(-0.377883);
c3 = rnd(-0.360608);
c4 = rnd(-0.142123);

y0 rnd= (((((c0*x0)+(c1*x1))+(c2*x2))+(c3*x3))+(c4*x4));
My0 = (((((-0.793176*x0)+(0.154365*x1))+(-0.377883*x2))+(-0.360608*x3))+(-0.142123*x4));

{ x0 in [-1e+10, 1e+10] /\
  x1 in [-1e+10, 1e+10] /\
  x2 in [-1e+10, 1e+10] /\
  x3 in [-1e+10, 1e+10] /\
  x4 in [-1e+10, 1e+10]
    -> |y0 - My0| in ? }

#$ x2, x3, x4 in 5;
